package sketch.specs.symbc;

import java.io.File;
import java.util.LinkedList;
import java.util.List;
import java.util.Map;

import gov.nasa.jpf.symbc.SolvedPCResults;
import sketch.jpf.symbc.SymbolicJPF;
import sketch.main.CodeToolkit;
import sketch.util.Globals;
import jpftreemap.TreeMap;
import jpftreemap.TreeMapTest_testRemove;
import junit.framework.Test;
import junit.framework.TestCase;
import junit.framework.TestSuite;

public class SymbolicJPFTest extends TestCase {
	
	public static Test suite() {
		return new TestSuite(SymbolicJPFTest.class);
	}
	
	public void testSymbolicMyClass1() {
		SymbolicJPF.execute(MyClass1.class, MyClass1.class, "myMethod");
		List<Map<String, Integer>> solvedIntValues = SolvedPCResults.solvedIntValues;
		String result = solvedIntValues.toString();
		System.out.println("Solved results are: " + solvedIntValues);
		assertTrue(solvedIntValues.size() == 2);
		//assertEquals("[{x_1_SYMINT=10000, y_2_SYMINT=-9999}, {x_1_SYMINT=-10000, y_2_SYMINT=-10000}]", result);
		SolvedPCResults.reset();
	}
	
	public void testSymbolicMyClass1ByReflection() {
		SymbolicJPF.execute(MyClassReflection1.class, MyClass1.class, "myMethod");
		System.out.println(SolvedPCResults.solvedIntValues.toString());
		assertTrue(SolvedPCResults.solvedIntValues.isEmpty());
	}
	
	//note that the output dir MUST be put into your classpath
	public void notfixed_testSymbolicClassLoadFromDir() {
		List<File> sources = new LinkedList<File>();
		sources.add(new File("./testfiles/sketch/specs/symbc/MyClassFromDir.java"));
		CodeToolkit.compile(sources, Globals.getClasspath(), "Compiling...");
		
		Class<?> clazz = CodeToolkit.loadClassFromDir("./testfiles/sketch/specs/symbc", "MyClassFromDir");
		//see the class
		System.out.println(clazz);
		System.out.println("Now try symbolic execution on that clazz: " + clazz.getName());
		//do symbolic execution
		if(clazz == null) {
			throw new RuntimeException("Can not load MyClassFromDir");
		}
		SymbolicJPF.execute(clazz, clazz, "myMethod");
		List<Map<String, Integer>> solvedIntValues = SolvedPCResults.solvedIntValues;
		String result = solvedIntValues.toString();
		System.out.println("Solved results are: " + solvedIntValues);
	}
}